This invention relates to very large scale integrated circuit design, testing and verification, and more particularly to systems and methods for determining variable orders for ordered binary decision diagrams.
Binary decision diagrams (BDDs) have been used to solve CAD related problems. These problems include synthesis problems, digital-system verification, protocol validation, and generally verifying the correctness of circuits. BDDs represent Boolean functions. For example, FIG. 1 shows a circuit comprising first and second OR gates 11, 13, and an AND gate 15. The first OR gate has inputs N1 and N2. The second OR gate has inputs N2 and N3, with input N2 being shared by the two OR gates. The outputs of the OR gates are fed into the AND gate. The AND gate has an output N6. Thus, the output of the AND gate can be represented by the Boolean function N6=(N1 OR N2) AND (N2 OR N3).
A BDD for this circuit is shown in FIG. 2. The BDD is composed of nodes, which may also be called vertices, and branches. Nodes from which no further branches extend are termed terminal nodes or terminals. The BDD is an Ordered BDD (OBDD) as each input is restricted to appearing only at one level of the BDD. The BDD may be reduced to a Reduced OBDD (ROBDD) as shown in FIG. 3. The rules for reducing OBDDs are known in the art. The importance of ROBDDs is that ROBDDs are unique, i.e., canonical. Thus, if two OBDDs reduce to the same ROBDD, the function of the circuits represented by the OBDDs are equivalent.
In most applications, ROBDDs are constructed using some variant of the Apply procedure described in R. E. Bryant, Graph-Based Algorithms For Boolean Function Manipulation, IEEE Trans. Computer C-35(8): 667-691, August 1986, the disclosure of which is incorporated by reference herein. Using the Apply procedure, the ROBDD for a gate g is synthesized by the symbolic manipulation of the ROBDDs of gate g""s inputs. Given a circuit, the gates of the circuit are processed in a depth-first search manner until the ROBDDs of the desired output gates are constructed.
A large number of problems in VLSI-CAD and other areas of computer science can be formulated in terms of Boolean functions. Accordingly, ROBDDs are useful for performing equivalence checks. A central issue, however, in providing computer aided solutions and equivalence checking is to find a compact representation for the Boolean functions so that the equivalence check can be efficiently performed. ROBDDs are efficiently manipulable, and as previously stated, are canonical. In many practical functions ROBDDs are compact as well, both in terms of size (memory space) and computational time. Accordingly, ROBDDs are frequently used as the Boolean representation of choice to solve various CAD problems.
ROBDDs, however, are not always compact. In a large number of cases of practical interest, many ROBDDs representing a circuit or system described by a Boolean function may require space which is exponential in the number of primary inputs (PIs) to the circuit or system. This makes solving for equivalence an NP-hard problem. The large space requirement, either in terms of memory or computational time, places limits on the complexity of problems which can be solved using ROBDDs.
The size of a BDD depends on, among other items, the order in which variables are evaluated. For example, the Boolean function a1xc2x7b1+a2xc2x7b2+a3xc2x7b3 can be represented by an eight node BDD using a variable order a1, b1, a2, b2, a3, b3. Using a variable order of a1, a2, a3, b1, b2, b3, however, results in a BDD with sixteen nodes. Determining a good variable order is a non-trivial problem. In fact, determining the optimal variable order of an n variable function, which has as many as n! different orders of input variables, is an NP-complete problem.
Approaches to determining good variable orders can be divided into two groups, static approaches and dynamic approaches. In a static approach, a variable order is determined and then used throughout the process of building a BDD. In a dynamic approach the variable order changes during the building the BDD.
Often in a static approach a variable order is determined using a depth-first search or breadth-first search to determine topological closeness of variables. In other words, variables are chosen in the manner in which they appear to be most naturally grouped together in the structural description of a circuit. Static approaches, however, are often largely unsuccessful. One reason for the lack of success of static ordering approaches is that they do not conduct adequate analysis of the function.
Dynamic approaches make use of the fact that BDDs are generally built beginning from primary inputs and extending, node by node, to a primary output. In other words, intermediate BDDs are built for each node of the circuit, until finally the BDD for a primary output is built. In a dynamic approach, variable orders are permutated at the intermediate nodes such that some cost function (often the size of the resulting BDD) is minimized. An example of a dynamic approach is a sifting based approach. In a sifting based dynamic ordering scheme, a variable is successively moved (sifted) to each position in the ordering list, and a different BDD is built for each variable ordering. The variable is then assigned the position in the variable ordering which results in a smallest graph size. The process is then repeated for each variable in the graph.
Dynamic variable ordering approaches are, however, often unsuccessful. One problem is that the sifting approach may result in a variable ordering which, due to the mechanics of dynamic reordering, constrain the possible variable ordering to variable orders which will not result in a small size BDD. For example, in a sifting based dynamic reordering scheme sifting of a variable in one direction in the variable order may be halted if the sifting is resulting in progressively larger BDD sizes. In such a scheme the variable, or a set of variables, is essentially constrained within a band of positions in the variable order because positions immediately outside of the band result in larger BDDs. However, significantly greater shifting of the variable may result, at some point, in a BDD significantly smaller than the BDDs possible with the variable constrained to the band of positions. Thus, depending on the function and the initial variable order used, a BDD for the function may be trapped at a size representing a local minima in size, which may be too large to effectively build, even if a small size BDD could be built for the function. In addition, even when the sifting approach results in a final, small sized BDD, the sifting approach may take an excessive amount of time to perform variable reordering.
Furthermore, dynamic reordering techniques cannot be used in all applications. For example, some alternative BDD representations, such as GBDDs, IBDDs, and XBDDs, require that the variable order must not change during the building of a BDD. Further, some test generation applications and SAT-solvers place great importance on determining the order of input variables used to begin a search. Accordingly, there is a need for determining good static variable orders, as well as a need for determining good initial variable orders for dynamic reordering packages.
The present invention provides a method of determining a variable order for building a binary decision diagram for a Boolean function forming a Boolean space, the Boolean function representing a circuit design. In one form, the method comprises forming samples of the Boolean space representing the Boolean function, building test binary decision diagrams for the samples using a plurality of test variable orders, and determining the variable order for building the BDD using information regarding the size of the test BDDs. In one embodiment the samples of the Boolean space are formed by using partial assignments. In another embodiment the samples of the Boolean space are formed using abstract BDDs. In another embodiment the samples of the Boolean space are created using decomposed BDDs. In another embodiment the samples of the function are created using smaller portions of the circuit.
In forming the Boolean subspaces, parameters are used to influence the formation of the samples. These parameters include parameters relating to a set of primary input variables used for abstraction and in one embodiment the set of primary input variables is determined by simulating a portion of a circuit design. The parameters estimated in another embodiment are a set of decomposition points which may be determined randomly, when a BDD goes beyond a threshold value, or when a BDD operation exceeds a predetermined computer resource amount.
The present invention also provides a method of building BDDs representing a Boolean function, the Boolean function defining the Boolean space of a circuit design. In one embodiment the method preprocesses a circuit design by examining a plurality of subspaces of the Boolean space, determines a variable order based on examination of the Boolean subspace, and builds a BDD representing the Boolean function using the variable order of an initial variable order.
Many of the attendant features of this invention will be more readily appreciated as the same becomes better understood by reference to the following detailed description and considered in connection with the accompanied drawings in which like reference symbols designate like parts throughout.